$\forall$$E$, $A$:Type, ${\it info}$:($E$$\rightarrow$((:Id $\times$ $A$) + (:(:IdLnk $\times$ $E$) $\times$ Id))), $e$:$E$.
\\[0ex]($\uparrow$rcv?($e$)) $\Rightarrow$ (rtag(${\it info}$;$e$) $\in$ Id)